Section: Scientific Foundations

Relevant techniques

The formal methods relevant to Licit include (1) specification methods and (2) validation methods.

1. Specifications are models or abstract representations of IT systems and their properties which can be used to define their expected behaviour without ambiguity. Specifications can also serve as a basis for various kinds of analyses and tools such as consistency analysis, validation, evaluation, certification, and animation. Specifications can play a role at different phases of the life cycle of a system : before, during or after its design and development. Different specification frameworks have been proposed, which can be roughly classified into semi-formal methods and formal methods. Semi-formal methods provide a well-defined syntax for the models (or “views” of the models) while the underlying semantics remain informal; in contrast, formal methods rely on a mathematical framework which is used to define the semantics of the models. The benefit of semi-formal methods is the definition of a shared body of notions, presentation rules and graphical tools which improve the communication and mutual understanding between the actors involved in the life-cycle of a system (designer, architect, development teams, evaluators, etc.). However, because of their lack of mathematical semantics, they do not necessarily guarantee the absence of ambiguity and they are not supported by formal verification tools. A standard example of semi-formal framework is UML. In contrast, formal methods such as Coq or B come with interactive theorem provers which help users verifying critical properties of their models. In addition, they provide ways to establish a formal link between a model and its implementation (through program extraction in Coq and refinement in B). Both formal and semi-formal methods are relevant to Licit , especially specification techniques based on “execution traces” where the expected behaviour of a system is defined in terms of properties of its sequences of operations. As far as logical frameworks are concerned, temporal logics (which make it possible to express properties on the future or the past) and deontic logics (which involve obligation and permission operators) are of prime importance in specifying legal rules.

2. Validation consists in checking a system to ensure that it behaves as expected. The most ambitious validation methods involve a formal specification of the system (using one of the aforementioned formalisms) and a proof (usually interactive) that the actual implementation complies with the specification. An alternative approach is to use the formal specification to derive test suites in a systematic way based on well-defined coverage criteria. The validation can also consist of checking simpler properties (typically well-foundedness properties such as type correctness, absence of buffer overflow or implementation of specific security properties) using automatic tools: these tools are called “type checkers” when the properties to be checked are expressed as types and “program analysers” when they are defined in terms of abstract domains. The main benefit of this category of tools is their automation; their limitation is the restricted expressive power of their language of properties. For Licit , a posteriori verifications are as relevant as a priori verifications: a posteriori checks are necessary when a priori verifications are either insufficient or not feasible, which is the case in particular for obligations which cannot be enforced by technical means.

To conclude this subsection, we stress the fact that the separations into categories (semi-formal versus formal, type inference versus program analysis, testing versus verification) have been used for the sake of the presentation (and because they originated from different research communities) but the frontiers between them tend to blur: for example certain frameworks include semi-formal and formal techniques, graphical representations such as state diagrams can be endowed with formal semantics, types can be defined in terms of abstract domains, program analysers can themselves be checked by theorem provers, etc.